perm filename NOTES.THE[LSP,JRA] blob
sn#254381 filedate 1976-12-17 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00003 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 To describe the evaluation of a function-call in LISP we must add
C00007 00003 .NEXT PAGE
C00021 ENDMK
C⊗;
To describe the evaluation of a function-call in LISP we must add
an equation to %9D%4e%1:
.BEGIN TABIT1(15);FILL;TURN ON "#";
\%9D%4e%f(%af%1[%as%41%1,#...,%as%4n%1]%f)%d(l)%1#=#
%9D%4a%f(%af%f)%d(l)(%9D%4e%f(%as%41%f)%d(l)%1,#...,%9D%4e%f(%as%4n%f)%d(l))%1
.END
We must also make consistent modifications to the previous clauses of %9D%4tgr%1 to
account for environments.
That is, the value of a constant is independent of the
specific environment in which it is evaluated.
.BEGIN TURN OFF "{","}";TURN ON "#";center;
%9D%4e%1{%as%*}(%dl%*)#=#%ds%*.
.END
A similar modification must be made for
conditional expressions.
Before we get very far in applying functions to values
we must give a mathematical characterization of function definitions.
In this section we will handle
handle λ-notation without free variables, postponing more complex
cases to {yonss(P90)}.
Assuming the only free variables in %9x%* are among the %3x%4i%*'s
the denotation of %3λ[[x%41%*, ..., x%4n%*] %9x%1] in a specified
environment should be a function
from %aS%8n%1 to %aS%* such that:
.BEGIN TABIT1(15);FILL;TURN ON "#";
\%9D%4a%f(%3λ[[%av%41%1,#...#%av%4n%1]%as%1]%f)%d(l)%1#=#
%d%9λ%d(x%41%*,#...,#%dx%4n%*)%9D%4e%f(%as%f)%d(l#:#<x%41%*,%dv%41%d>,#...,#<x%4n%*,%dv%4n%d>)%1
.END
where λ is the LISP λ-notation and %9λ%* is its mathematical counterpart and
%dv%4i%1 is the denotational counterpart of %av%4i%1.
In more detail:
%9λ%d(x%41%*, ... ,x%4n%*)e(x%41%*, ... ,x%4m%*) %1is a function %df%*: %aS%8n%1 → %aS%* such that:
.BEGIN TABIT1(15);GROUP;
\ | is %de(t%41%*, ... ,t%4n%*) %1if m%c≥%*n and %c∀%*i%dt%4i%1 %c≠%* %9B%1.
%df(t%41%*, ... t%4m%*) %1\<
\ | is %9B%* otherwise
.END
Also, %d(l#:#<x%41%*,%dv%41%d>,#...,#<x%4n%*,%dv%4n%d>)%1 is a modification
of %dl%* such that each %dv%4i%1 is bound to the corresponding %dx%4i%1.
.BEGIN TABIT2(20,40);GROUP;
That is:\%d(l#:#<x,v>)%1 is: %9λ%d(v%41%*)%2\if %dv = %9B%* %2then %9B%2
\\else if %dv%41%* = %9B%2 then %9B%2
\\else if %dv%41%* = x%2 then %dv%2
\\else %dl(v%41%*)%1.
where: %2if%d p%* then %dq%* else %dr%1 is %dif(p,q,r)%1.
.END
After all this work there really should be a comparable return on
on our investment. An immediate benefit is
clearer understanding of the differences between mathematics and programming
languages and a
clearer perception of the role of definition and computation.
It should raise questions about the class of objects called function
and the class of objects called procedures.
We know that the LISP %3label%1 operator is similar to "<=", but
%3label%1 builds a temporary definition, while "<=" modifies the
environment. Programming language constructs which modify the environment
are said to have %2side-effects%1 and are an instance
of what is called a imperative construct.
The next chapter introduces the procedural aspects of
imperative constructs and in {yonss(P90)}
we will investigate some of the mathematical aspects of
"<=" and %3label%1.
.NEXT PAGE;
.<<to raproachment???>>
We can give some insight into the mathematical properites of
%3label%1.
As before, we take our clues from the behavior of %3eval%* and %3apply%*.
In any environment %9D%4a%1 should map %3label[f;g]%* in such a way that the
denotation of %3f%* is synonymous with that of %3g%*.
That is, %df%* is a mapping satisfying the equation
%df(t%4i%*,#...,#t%4n%*)#=#%dg(t%4i%*,#...,#t%4n%*)%1.
So:
.BEGIN CENTERIT;FILL;TURN ON "#";
←%9D%4a%f(%3label[%af%1;%ag%1]%f)%d(l)%1#=#%9D%4a%f(%ag%f)%d(l)%1.
.END
This will suffice for our current λ-definitions; we need not modify %dl%*
since the name %3f%* will never be used within the evaluation of
an expression involving %3g%*.
.BEGIN TURN ON "#";
We must be a bit careful.
Our treatment of evaluation of free
variables in LISP (on {yon(P93)} and in {yonss(P77)}) shows that free
variables in a function are to be evaluated when the function is %2activated%*
rather than when
the function is defined. Thus a λ-definition generally
requires an environment in which to evaluate its free variables.
So its denotation
should be a mapping like: %denv%*#→#[%aS%8n%1#→#%aS%*] rather than
simply %aS%8n%1#→#%aS%1. This is consistent with our understanding of the
meaning of λ-notation.
It is what %3function%* was attempting to
describe.
What we previously have called an ⊗→open function↔← is of the
form:
%aS%8n%1#→#%aS%*.
.END
This view of λ-notation must change our conception on %denv%* as well.
Given a name for a function in an environment we can expect to receive
a mapping from %denv%* to an element of %aFn%*. That is, for such names:
.BEGIN CENTERIT;
←%denv %1is the set of functions: %aId%1 → [%denv%1 → %aFn%1]
.END
A modification of our handling of %3label%* seems to describe the case
for recursion:
.BEGIN CENTERIT;FILL;TURN ON "#";
←%9D%4a%f(%3label[%af%1;%ag%1]%f)%d(l)%1#=#%9D%4a%f(%ag%f)%d(l#:#<f,%9D%4a%f(%ag%f)%d>)%1.
.END
Interpreting this equation operationally, it says: when we apply a %3label%*
expression in an environment it is the same as applying the body of the definition
in an environment modified to associate the name with its definition.
This is analogous to what the LISP %3apply%* function will do.
Recalling the inadequacy of this interpretation of %3label%* in more
general contexts ({yon(P94)}),
we should perhaps look further for a general reading of %3label%*. Our hint
comes from our interpretation of "<=" as an equality. I.e., recall:
.BEGIN CENTER;SELECT 3;TURN OFF "←";
fact ← %1a solution to the equation:%* f = λ[[x][x=0 → 1; %et%3 → *[x;f[x-1]]]].
.END
What we need is a representation of an "equation-solver" which will
take such an equation and will return a function
which satisfies that equation. In particular we would like the %2best%*
solution in the sense that it imposes the minimal structure on the function⊗↓Like
a free group satisfies the group axioms, but imposes no other
requirements.←.
This request for minimality translates to finding the function which
satisfies the equation, but is least-defined on other elements of the
domain. This discussion of "least" brings in the recent work of D. Scott
and the intuition behind
this study again illuminates the distinction
between mathematical meaning (denotational) and manipulative meaning (operational).
Consider the following LISP definition:
.BEGIN CENTER;SELECT 3;
f <= λ[[n][n=0 → 0; %et%3 → f[n-1] + 2*n -1]]
.END
.BEGIN TURN ON "#";
When we are asked what this function is doing, most of us would proceed
operationally; that is, we would begin computing %3f[n]%* for different
values of %3n%* --what#is#%3f[0]?%*,
what is %3f[1]%1,#...#. It is profitable to look at this process differently:
what we are doing is looking at a %2sequence%* of functions,
call them %df%4i%1's .
.END
.BEGIN TABIT3(10,16,44);SELECT d;GROUP;TURN OFF "{","}";
\f%40%1 =\%d{<0,%9B%*>,<1,%9B%*>, ... }\%1when we begin, we know nothing.
\%df%41%1 =\%d{<0,0>,<1,%9B%*>, ... }\%1now we know one pair.
\%df%42%1 =\%d{<0,0>,<1,1>, ... }\%1now two
\%df%43%1 =\%d{<0,0>,<1,1>,<2,4>, ... }\%1now three
\ ...\ ... ...\%dEureka!!
.END
When (if) the sudden realization strikes us that the LISP function is
"really" (denotationally) %dn%82%1 on the non-negative integers,
then we may either take
that insight on faith or subject it to proof. The process of discovering
the denotation can be construed as a limiting process which creates
the least-defined function satisfying the LISP definition. That is:
.BEGIN CENTER;SELECT d;
%9λ%d((n)n%82%d)%1 = %1least upper bound of%d f%4i%1's;
.END
where %df%4i%1 may also be characterised as:
.BEGIN TABIT1(12);SELECT D;group;
\ %1|%d n%82%1 if %d0%c≤%dn%c≤%di
f%4i%d(n)%1 =\<
\ | %9B%1 if %di%c<%dn
.END
We may think of our "equation-solver" as proceeding in such a manner.
Though it is not at all obvious, such an equation solver
%2does%* exist; it is called the %2⊗→fixed-point operator↔←%* and is
designated here by %dY%*. We will now give an intuitive derivation of %dY%*.
In terms of our example we want a solution to %df = %9t%d(f)%1, where:
.BEGIN CENTER;
%9t%d(g) = %9λ%d((n) cond(n=0, 0, g(n-1)+2*n-1))%1,
.END
Our previous discussion leads us to believe that
%9λ%d((n)n%82%d) %1for %dn %c≥%d0%1 is the desired solution.
.BEGIN TURN ON "#";
How does this discussion relate to the sequence of functions %df%4i%1?
First, it's important to keep the domains of our various mapping in mind:
%df%*#%9ε%*#Fn and %9t%* is a functional in %aFn%1#→#%aFn%1.
Let's look at the behavior of %9t%* for various
arguments. The simplest function is the totally undefined function, %9B%*#⊗↓We
perhaps should subscript %9B%* to distinguish it from previous %9B%*'s.←.
.BEGIN CENTER;
%9t%d(%9B%d) = %9λ%d((n) cond(n=0, 0, %9B%*(n-1)+2*n-1))%1,
.END
but this says %9t%d(%9B%*)%1 is just %df%41%1!
Similarly,
.BEGIN CENTER;
%9t%d(%9t%d(%9B%*))#=#%9λ%d((n) cond(n=0, 0, f%41%*(n-1)+2*n-1))%1,
.END
is just %df%42%1.
Thus, writing %9t%8n%1 for the composition of %9t%1...%9t%1, n times, ⊗↓Define
%9t%80%1 to be the the totally undefined function, %9B%1.← we can say
.BEGIN CENTER;GROUP;
%df%4n%* = %9t%8n%d(%9B%*)%1 or,
%9λ%d((n)n%82%*)%1 = lim%4n=0 → ∞%9t%8n%d(%9B%d)%1.
.END
Or in general the fixed-point of an equation %df = %9t%*(f)%1 satisfies the
relation:
.BEGIN CENTER;
%dY(%9t%*) = lim%4n→∞%9t%8n%d(%9B%d).%1
.END
Thus in summary, %dY%* is a mapping: %d[[%aFn%* → %aFn%*] → %aFn%*]%1
such that if %9t%*#%9ε%d#[%aFn%*#→#%aFn%*]%1 and %df%*#=#%9t%d(f)%1, then
%9t%d(Y(%9t%*))%1#=#%dY(%9t%*)%1 and %dY(%9t%*)%1 is least-defined of any of the solutions
to %df%*#=#%9t%d(f)%1.
.END
So the search for denotations for %3label%* might be better served by:
.BEGIN CENTERIT;FILL;TURN ON "#";
←%9D%4a%f(%3label[%af%1;%ag%1]%f)%d(l)%1#=
#%dY(%9λ%d(h)%9D%4a%f(%ag%f)%d(l%1#:#%d<f,h>))%1.
.END
The characterizations are %2not%* the same. Examination of the
behavior of %9D%4e%f(%3label[car;car][(A#B)]%f)%1 will exhibit a discrepancy.
Which characterization of %3label[f;g]%* is "better"?
The first denotation parallels the behavior of %3eval%* and %3apply%*, applying
%3g%* in a %denv%* modified by the pair %d<f,g>%*.
The later fix-point characterization says %3label[f;g]%* is a particular
solution the the equation %df#=#g%*. As we have seen, the "meaning" of %3label%*
is better served by this fix-point interpretation. The crucial questions, however,
are: first, are these two denotations different?
And which, if either, interpretation is %2correct%*?
That is, which
characterization has the same %2effect%* as %3eval%* and %3apply%*?
The general question of the correctness of the denotational semantics which we
are developing is the subject of much of M. Gordon's thesis.
The intuitions presented in this section can be made very precise.
The natural ordering
of "less defined" exemplified by the sequence of %df%4i%1's: %df%4i%1 is less
defined (or approximates) %df%4j%1, j%c≥%1i, imposes a structure on our domain of functions.
Indeed, a structure can be naturally superimposed on all of our domains.
If we require that some additional simple properties hold on our domains, then
the intuitions of this section can be justified mathematically.
*** ADD MONOTONICITY, CONTINUITY
***** continuations and models for imperatives****